Issue5410-3.agda:7,3-4
{@0 A : Set} → A → D is not usable at the required modality
when checking that the type {@0 A : Set} → A → D of the constructor
c fits in the sort Set₁ of the datatype.
